package edu.cmu.cs.erl.unitTests;

import java.util.ArrayList;
import java.util.List;

import jp.ac.kobe_u.cs.prolog.lang.JavaObjectTerm;
import jp.ac.kobe_u.cs.prolog.lang.Term;
import jp.ac.kobe_u.cs.prolog.lang.VariableTerm;

import org.junit.Assert;
import org.junit.Test;

import edu.cmu.cs.erl.ERL;
import edu.cmu.cs.erl.ERLError;
import edu.cmu.cs.erl.ERLException;
import edu.cmu.cs.erl.Oracle;
import edu.cmu.cs.erl.TermBuilder;



public class ForallTest {
	@Test
	public void sizeOneList() throws ERLException {
		Oracle oracle = new TestOracle();
		
		VariableTerm X = oracle.getVariable("X");
		Term term1 = TermBuilder.createAtomicTerm(X);
		Term term2 = TermBuilder.createAtomicTerm("a");
		Term andTerm = TermBuilder.createAndTerm(term1, term2);
		
		ArrayList<String> list = new ArrayList<String>();
		list.add("a");
		
		Term forAll = TermBuilder.createForAllTerm(oracle,list,"X",andTerm);
		List<ERLError> errors = ERL.runPredicate(oracle, forAll, true);
		
		Assert.assertTrue(errors.isEmpty());
	}
	
	@Test
	public void sizeManyListAllTrue() throws ERLException {
		Oracle oracle = new TestOracle();
		
		VariableTerm X = oracle.getVariable("X");
		Term term1 = TermBuilder.createAtomicTerm(X);
		Term term2 = TermBuilder.createAtomicTerm("a");
		Term andTerm = TermBuilder.createAndTerm(term1, term2);
		
		ArrayList<String> list = new ArrayList<String>();
		list.add("a");
		list.add("a");
		list.add("a");
		
		Term forAll = TermBuilder.createForAllTerm(oracle, list,"X",andTerm);
		List<ERLError> errors = ERL.runPredicate(oracle, forAll, true);
		
		Assert.assertTrue(errors.isEmpty());
	}
	
	@Test
	public void sizeManyList() throws ERLException {
		Oracle oracle = new TestOracle();
		
		VariableTerm X = oracle.getVariable("X");
		Term term1 = TermBuilder.createAtomicTerm(X);
		Term term2 = TermBuilder.createAtomicTerm("a");
		Term andTerm = TermBuilder.createAndTerm(term1, term2);
		
		ArrayList<String> list = new ArrayList<String>();
		list.add("a");
		list.add("b");
		list.add("c");
		
		Term forAll = TermBuilder.createForAllTerm(oracle,list,"X",andTerm);
		List<ERLError> errors = ERL.runPredicate(oracle, forAll, true);
		
		Assert.assertEquals(1, errors.size());
		Assert.assertEquals("b", errors.get(0).getOwner());
	}
	

	
	@Test
	public void nestedForAll() throws ERLException {
		Oracle oracle = new TestOracle();
		
		VariableTerm X = oracle.getVariable("X");
		VariableTerm Y = oracle.getVariable("Y");
		Term term1 = TermBuilder.createAtomicTerm(X);
		Term term2 = TermBuilder.createAtomicTerm(Y);
		Term andTerm = TermBuilder.createAndTerm(term1, term2);
		
		ArrayList<String> list = new ArrayList<String>();
		list.add("a");
		list.add("b");
		
		ArrayList<String> list2 = new ArrayList<String>();
		list2.add("c");
		list2.add("d");
		
		Term innerforallTerm = TermBuilder.createForAllTerm(oracle, list2,"X",andTerm);
		Term outterforallTerm = TermBuilder.createForAllTerm(oracle, list,"Y",innerforallTerm);
		List<ERLError> errors = ERL.runPredicate(oracle, outterforallTerm, true);
		
		Assert.assertEquals(4, errors.size());
		Assert.assertEquals("d", errors.get(0).getOwner());
		Assert.assertEquals("c", errors.get(1).getOwner());
		Assert.assertEquals("d", errors.get(2).getOwner());
		Assert.assertEquals("d", errors.get(3).getOwner());
		
	}
	
	@Test
	public void manyAllFail() throws ERLException {
		Oracle oracle = new TestOracle();
		
		VariableTerm X = oracle.getVariable("X");
		Term term1 = TermBuilder.createAtomicTerm(X);
		Term term2 = TermBuilder.createAtomicTerm("a");
		Term andTerm = TermBuilder.createAndTerm(term1, term2);
		
		ArrayList<String> list = new ArrayList<String>();
		list.add("b");
		list.add("b");
		
		Term forAll = TermBuilder.createForAllTerm(oracle,list,"X",andTerm);
		List<ERLError> errors = ERL.runPredicate(oracle, forAll, true);
		
		Assert.assertEquals(2, errors.size());
		Assert.assertEquals("b", errors.get(0).getOwner());
		Assert.assertEquals("b", errors.get(1).getOwner());
	}
	
	@Test
	public void checkLazyLoading() throws ERLException {
		Oracle oracle = new TestOracle();
		
		VariableTerm X = oracle.getVariable("X");
		Term term1 = TermBuilder.createAtomicTerm(X);
		Term term2 = TermBuilder.createAtomicTerm("a");
		Term andTerm = TermBuilder.createAndTerm(term1, term2);
		
		ArrayList<String> list = new ArrayList<String>();
		list.add("a");
		list.add("b");
		list.add("a");
		
		Term forAll = TermBuilder.createForAllLazyTerm(oracle,list,"X",andTerm);
		List<ERLError> errors = ERL.runPredicate(oracle, forAll, true);
		
		Assert.assertEquals(1, errors.size());
		Assert.assertEquals("b", errors.get(0).getOwner());
	}
}